$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, ${\it ds}$:fpf(Id; $x$.Type).
\\[0ex]@$i$ discrete ${\it ds}$ $\Rightarrow$ subtype\_rel(es{-}state(${\it es}$; $i$); decl{-}state(${\it ds}$))